ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple{i:l}(ds; da), n:,
L:(event-info(ds;da) List), k:Knd, s:decl-state(ds), v:ma-valtype(da; k).
(ecl-trans-act(ds; da; A)(n,append(L; cons(<k, s, v>; []))))
 ((k  ecl-trans-ks(A)) c ((ecl-trans-a(A)(n,k,s,v,ecl-trans-state(A; L))))) 

latex

Definitions

t  T, ma-valtype(da; k), P  Q, False, A, A  B, , x:A. B(x), ecl-trans-state(v; L), ecl-trans-ks(v), Knd, (x  l), ecl-trans-a(v), b, A c B, event-info(ds;da), spreadn(a; x,y,z.t(x;y;z)), top, fpf-cap(f; eq; x; z), Kind-deq, x. t(x), decl-state(ds), subtype(S; T), append(as; bs), P  Q, x:A. B(x), ecl-trans-act(ds; da; A), guard(T), sq_type(T), prop{i:l}, True, T, Id, fpf(A; a.B(a)), ecl-trans-tuple{i:l}(ds; da), ecl-trans-type(A), , t.1, t.2, P  Q, ||as||, P  Q, P  Q

Lemmas

ecl-trans-act wf, ma-valtype wf, nat wf, general-append-cancellation, length wf1, cons one one, pi2 wf, pi1 wf, bool wf, squash wf, true wf, ecl-trans-tuple wf, fpf wf, Id wf, Knd sq, append wf, event-info wf, decl-state wf, fpf-cap wf, Kind-deq wf, top wf, assert wf, ecl-trans-a wf, l member wf, Knd wf, ecl-trans-ks wf, ecl-trans-state wf